0 CpxTRS
↳1 TrsToWeightedTrsProof (BOTH BOUNDS(ID, ID), 0 ms)
↳2 CpxWeightedTrs
↳3 TypeInferenceProof (BOTH BOUNDS(ID, ID), 4 ms)
↳4 CpxTypedWeightedTrs
↳5 CompletionProof (UPPER BOUND(ID), 0 ms)
↳6 CpxTypedWeightedCompleteTrs
↳7 CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID), 0 ms)
↳8 CpxRNTS
↳9 CompleteCoflocoProof (⇔, 2551 ms)
↳10 BOUNDS(1, n^2)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
inc(0) → 0
inc(s(x)) → s(inc(x))
minus(0, y) → 0
minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
quot(0, s(y)) → 0
quot(s(x), s(y)) → s(quot(minus(x, y), s(y)))
log(x) → log2(x, 0)
log2(x, y) → if(le(x, 0), le(x, s(0)), x, inc(y))
if(true, b, x, y) → log_undefined
if(false, b, x, y) → if2(b, x, y)
if2(true, x, s(y)) → y
if2(false, x, y) → log2(quot(x, s(s(0))), y)
le(0, y) → true [1]
le(s(x), 0) → false [1]
le(s(x), s(y)) → le(x, y) [1]
inc(0) → 0 [1]
inc(s(x)) → s(inc(x)) [1]
minus(0, y) → 0 [1]
minus(x, 0) → x [1]
minus(s(x), s(y)) → minus(x, y) [1]
quot(0, s(y)) → 0 [1]
quot(s(x), s(y)) → s(quot(minus(x, y), s(y))) [1]
log(x) → log2(x, 0) [1]
log2(x, y) → if(le(x, 0), le(x, s(0)), x, inc(y)) [1]
if(true, b, x, y) → log_undefined [1]
if(false, b, x, y) → if2(b, x, y) [1]
if2(true, x, s(y)) → y [1]
if2(false, x, y) → log2(quot(x, s(s(0))), y) [1]
le(0, y) → true [1]
le(s(x), 0) → false [1]
le(s(x), s(y)) → le(x, y) [1]
inc(0) → 0 [1]
inc(s(x)) → s(inc(x)) [1]
minus(0, y) → 0 [1]
minus(x, 0) → x [1]
minus(s(x), s(y)) → minus(x, y) [1]
quot(0, s(y)) → 0 [1]
quot(s(x), s(y)) → s(quot(minus(x, y), s(y))) [1]
log(x) → log2(x, 0) [1]
log2(x, y) → if(le(x, 0), le(x, s(0)), x, inc(y)) [1]
if(true, b, x, y) → log_undefined [1]
if(false, b, x, y) → if2(b, x, y) [1]
if2(true, x, s(y)) → y [1]
if2(false, x, y) → log2(quot(x, s(s(0))), y) [1]
| le :: 0:s:log_undefined → 0:s:log_undefined → true:false 0 :: 0:s:log_undefined true :: true:false s :: 0:s:log_undefined → 0:s:log_undefined false :: true:false inc :: 0:s:log_undefined → 0:s:log_undefined minus :: 0:s:log_undefined → 0:s:log_undefined → 0:s:log_undefined quot :: 0:s:log_undefined → 0:s:log_undefined → 0:s:log_undefined log :: 0:s:log_undefined → 0:s:log_undefined log2 :: 0:s:log_undefined → 0:s:log_undefined → 0:s:log_undefined if :: true:false → true:false → 0:s:log_undefined → 0:s:log_undefined → 0:s:log_undefined log_undefined :: 0:s:log_undefined if2 :: true:false → 0:s:log_undefined → 0:s:log_undefined → 0:s:log_undefined |
le(v0, v1) → null_le [0]
inc(v0) → null_inc [0]
minus(v0, v1) → null_minus [0]
quot(v0, v1) → null_quot [0]
if2(v0, v1, v2) → null_if2 [0]
if(v0, v1, v2, v3) → null_if [0]
null_le, null_inc, null_minus, null_quot, null_if2, null_if
| Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules:
The TRS has the following type information:
Rewrite Strategy: INNERMOST |
0 => 0
true => 2
false => 1
log_undefined => 1
null_le => 0
null_inc => 0
null_minus => 0
null_quot => 0
null_if2 => 0
null_if => 0
if(z, z', z'', z1) -{ 1 }→ if2(b, x, y) :|: b >= 0, z1 = y, z = 1, x >= 0, y >= 0, z' = b, z'' = x
if(z, z', z'', z1) -{ 1 }→ 1 :|: z = 2, b >= 0, z1 = y, x >= 0, y >= 0, z' = b, z'' = x
if(z, z', z'', z1) -{ 0 }→ 0 :|: z1 = v3, v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0, v3 >= 0
if2(z, z', z'') -{ 1 }→ y :|: z = 2, z' = x, x >= 0, y >= 0, z'' = 1 + y
if2(z, z', z'') -{ 1 }→ log2(quot(x, 1 + (1 + 0)), y) :|: z' = x, z'' = y, z = 1, x >= 0, y >= 0
if2(z, z', z'') -{ 0 }→ 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0
inc(z) -{ 1 }→ 0 :|: z = 0
inc(z) -{ 0 }→ 0 :|: v0 >= 0, z = v0
inc(z) -{ 1 }→ 1 + inc(x) :|: x >= 0, z = 1 + x
le(z, z') -{ 1 }→ le(x, y) :|: z' = 1 + y, x >= 0, y >= 0, z = 1 + x
le(z, z') -{ 1 }→ 2 :|: y >= 0, z = 0, z' = y
le(z, z') -{ 1 }→ 1 :|: x >= 0, z = 1 + x, z' = 0
le(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
log(z) -{ 1 }→ log2(x, 0) :|: x >= 0, z = x
log2(z, z') -{ 1 }→ if(le(x, 0), le(x, 1 + 0), x, inc(y)) :|: x >= 0, y >= 0, z = x, z' = y
minus(z, z') -{ 1 }→ x :|: x >= 0, z = x, z' = 0
minus(z, z') -{ 1 }→ minus(x, y) :|: z' = 1 + y, x >= 0, y >= 0, z = 1 + x
minus(z, z') -{ 1 }→ 0 :|: y >= 0, z = 0, z' = y
minus(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
quot(z, z') -{ 1 }→ 0 :|: z' = 1 + y, y >= 0, z = 0
quot(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
quot(z, z') -{ 1 }→ 1 + quot(minus(x, y), 1 + y) :|: z' = 1 + y, x >= 0, y >= 0, z = 1 + x
| eq(start(V, V1, V17, V18),0,[le(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V17, V18),0,[inc(V, Out)],[V >= 0]). eq(start(V, V1, V17, V18),0,[minus(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V17, V18),0,[quot(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V17, V18),0,[log(V, Out)],[V >= 0]). eq(start(V, V1, V17, V18),0,[log2(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1, V17, V18),0,[if(V, V1, V17, V18, Out)],[V >= 0,V1 >= 0,V17 >= 0,V18 >= 0]). eq(start(V, V1, V17, V18),0,[if2(V, V1, V17, Out)],[V >= 0,V1 >= 0,V17 >= 0]). eq(le(V, V1, Out),1,[],[Out = 2,V2 >= 0,V = 0,V1 = V2]). eq(le(V, V1, Out),1,[],[Out = 1,V3 >= 0,V = 1 + V3,V1 = 0]). eq(le(V, V1, Out),1,[le(V4, V5, Ret)],[Out = Ret,V1 = 1 + V5,V4 >= 0,V5 >= 0,V = 1 + V4]). eq(inc(V, Out),1,[],[Out = 0,V = 0]). eq(inc(V, Out),1,[inc(V6, Ret1)],[Out = 1 + Ret1,V6 >= 0,V = 1 + V6]). eq(minus(V, V1, Out),1,[],[Out = 0,V7 >= 0,V = 0,V1 = V7]). eq(minus(V, V1, Out),1,[],[Out = V8,V8 >= 0,V = V8,V1 = 0]). eq(minus(V, V1, Out),1,[minus(V9, V10, Ret2)],[Out = Ret2,V1 = 1 + V10,V9 >= 0,V10 >= 0,V = 1 + V9]). eq(quot(V, V1, Out),1,[],[Out = 0,V1 = 1 + V11,V11 >= 0,V = 0]). eq(quot(V, V1, Out),1,[minus(V12, V13, Ret10),quot(Ret10, 1 + V13, Ret11)],[Out = 1 + Ret11,V1 = 1 + V13,V12 >= 0,V13 >= 0,V = 1 + V12]). eq(log(V, Out),1,[log2(V14, 0, Ret3)],[Out = Ret3,V14 >= 0,V = V14]). eq(log2(V, V1, Out),1,[le(V15, 0, Ret0),le(V15, 1 + 0, Ret12),inc(V16, Ret31),if(Ret0, Ret12, V15, Ret31, Ret4)],[Out = Ret4,V15 >= 0,V16 >= 0,V = V15,V1 = V16]). eq(if(V, V1, V17, V18, Out),1,[],[Out = 1,V = 2,V19 >= 0,V18 = V20,V21 >= 0,V20 >= 0,V1 = V19,V17 = V21]). eq(if(V, V1, V17, V18, Out),1,[if2(V22, V23, V24, Ret5)],[Out = Ret5,V22 >= 0,V18 = V24,V = 1,V23 >= 0,V24 >= 0,V1 = V22,V17 = V23]). eq(if2(V, V1, V17, Out),1,[],[Out = V25,V = 2,V1 = V26,V26 >= 0,V25 >= 0,V17 = 1 + V25]). eq(if2(V, V1, V17, Out),1,[quot(V27, 1 + (1 + 0), Ret01),log2(Ret01, V28, Ret6)],[Out = Ret6,V1 = V27,V17 = V28,V = 1,V27 >= 0,V28 >= 0]). eq(le(V, V1, Out),0,[],[Out = 0,V29 >= 0,V30 >= 0,V = V29,V1 = V30]). eq(inc(V, Out),0,[],[Out = 0,V31 >= 0,V = V31]). eq(minus(V, V1, Out),0,[],[Out = 0,V32 >= 0,V33 >= 0,V = V32,V1 = V33]). eq(quot(V, V1, Out),0,[],[Out = 0,V34 >= 0,V35 >= 0,V = V34,V1 = V35]). eq(if2(V, V1, V17, Out),0,[],[Out = 0,V36 >= 0,V17 = V37,V38 >= 0,V = V36,V1 = V38,V37 >= 0]). eq(if(V, V1, V17, V18, Out),0,[],[Out = 0,V18 = V39,V40 >= 0,V17 = V41,V42 >= 0,V = V40,V1 = V42,V41 >= 0,V39 >= 0]). input_output_vars(le(V,V1,Out),[V,V1],[Out]). input_output_vars(inc(V,Out),[V],[Out]). input_output_vars(minus(V,V1,Out),[V,V1],[Out]). input_output_vars(quot(V,V1,Out),[V,V1],[Out]). input_output_vars(log(V,Out),[V],[Out]). input_output_vars(log2(V,V1,Out),[V,V1],[Out]). input_output_vars(if(V,V1,V17,V18,Out),[V,V1,V17,V18],[Out]). input_output_vars(if2(V,V1,V17,Out),[V,V1,V17],[Out]). |
CoFloCo proof output:
Preprocessing Cost Relations
=====================================
#### Computed strongly connected components
0. recursive : [inc/2]
1. recursive : [le/3]
2. recursive : [minus/3]
3. recursive : [quot/3]
4. recursive : [if/5,if2/4,log2/3]
5. non_recursive : [log/2]
6. non_recursive : [start/4]
#### Obtained direct recursion through partial evaluation
0. SCC is partially evaluated into inc/2
1. SCC is partially evaluated into le/3
2. SCC is partially evaluated into minus/3
3. SCC is partially evaluated into quot/3
4. SCC is partially evaluated into log2/3
5. SCC is completely evaluated into other SCCs
6. SCC is partially evaluated into start/4
Control-Flow Refinement of Cost Relations
=====================================
### Specialization of cost equations inc/2
* CE 27 is refined into CE [34]
* CE 29 is refined into CE [35]
* CE 28 is refined into CE [36]
### Cost equations --> "Loop" of inc/2
* CEs [36] --> Loop 19
* CEs [34,35] --> Loop 20
### Ranking functions of CR inc(V,Out)
* RF of phase [19]: [V]
#### Partial ranking functions of CR inc(V,Out)
* Partial RF of phase [19]:
- RF of loop [19:1]:
V
### Specialization of cost equations le/3
* CE 26 is refined into CE [37]
* CE 24 is refined into CE [38]
* CE 23 is refined into CE [39]
* CE 25 is refined into CE [40]
### Cost equations --> "Loop" of le/3
* CEs [40] --> Loop 21
* CEs [37] --> Loop 22
* CEs [38] --> Loop 23
* CEs [39] --> Loop 24
### Ranking functions of CR le(V,V1,Out)
* RF of phase [21]: [V,V1]
#### Partial ranking functions of CR le(V,V1,Out)
* Partial RF of phase [21]:
- RF of loop [21:1]:
V
V1
### Specialization of cost equations minus/3
* CE 31 is refined into CE [41]
* CE 30 is refined into CE [42]
* CE 33 is refined into CE [43]
* CE 32 is refined into CE [44]
### Cost equations --> "Loop" of minus/3
* CEs [44] --> Loop 25
* CEs [41] --> Loop 26
* CEs [42,43] --> Loop 27
### Ranking functions of CR minus(V,V1,Out)
* RF of phase [25]: [V,V1]
#### Partial ranking functions of CR minus(V,V1,Out)
* Partial RF of phase [25]:
- RF of loop [25:1]:
V
V1
### Specialization of cost equations quot/3
* CE 15 is refined into CE [45]
* CE 17 is refined into CE [46]
* CE 16 is refined into CE [47,48,49]
### Cost equations --> "Loop" of quot/3
* CEs [49] --> Loop 28
* CEs [48] --> Loop 29
* CEs [47] --> Loop 30
* CEs [45,46] --> Loop 31
### Ranking functions of CR quot(V,V1,Out)
* RF of phase [28]: [V-1,V-V1+1]
* RF of phase [30]: [V]
#### Partial ranking functions of CR quot(V,V1,Out)
* Partial RF of phase [28]:
- RF of loop [28:1]:
V-1
V-V1+1
* Partial RF of phase [30]:
- RF of loop [30:1]:
V
### Specialization of cost equations log2/3
* CE 22 is refined into CE [50,51,52,53]
* CE 18 is refined into CE [54,55,56,57,58,59]
* CE 20 is refined into CE [60]
* CE 21 is refined into CE [61,62,63,64,65,66,67,68,69,70,71,72,73,74,75,76,77,78]
* CE 19 is refined into CE [79,80,81,82,83,84,85,86]
### Cost equations --> "Loop" of log2/3
* CEs [86] --> Loop 32
* CEs [82] --> Loop 33
* CEs [84,85] --> Loop 34
* CEs [80,81] --> Loop 35
* CEs [83] --> Loop 36
* CEs [79] --> Loop 37
* CEs [60] --> Loop 38
* CEs [58,59,69,70,77,78] --> Loop 39
* CEs [50,51,52,53] --> Loop 40
* CEs [54,55,56,57,61,62,63,64,65,66,67,68,71,72,73,74,75,76] --> Loop 41
### Ranking functions of CR log2(V,V1,Out)
* RF of phase [32,34]: [V-1]
* RF of phase [33,35]: [V-1]
#### Partial ranking functions of CR log2(V,V1,Out)
* Partial RF of phase [32,34]:
- RF of loop [32:1]:
V-2
- RF of loop [34:1]:
V-1
* Partial RF of phase [33,35]:
- RF of loop [33:1]:
V-2
- RF of loop [35:1]:
V-1
### Specialization of cost equations start/4
* CE 7 is refined into CE [87]
* CE 8 is refined into CE [88]
* CE 6 is refined into CE [89]
* CE 2 is refined into CE [90]
* CE 3 is refined into CE [91]
* CE 4 is refined into CE [92,93,94,95,96,97,98,99,100,101,102]
* CE 5 is refined into CE [103,104,105,106,107,108,109,110,111,112,113]
* CE 9 is refined into CE [114,115,116,117,118]
* CE 10 is refined into CE [119,120]
* CE 11 is refined into CE [121,122,123]
* CE 12 is refined into CE [124,125,126,127,128]
* CE 13 is refined into CE [129,130,131]
* CE 14 is refined into CE [132,133,134,135,136]
### Cost equations --> "Loop" of start/4
* CEs [124] --> Loop 42
* CEs [115,121] --> Loop 43
* CEs [87] --> Loop 44
* CEs [88] --> Loop 45
* CEs [89,134] --> Loop 46
* CEs [90,92,93,94,95,96,97,98,99,100,101,102,103,104,105,106,107,108,109,110,111,112,113] --> Loop 47
* CEs [91,114,116,117,118,119,120,122,123,125,126,127,128,129,130,131,132,133,135,136] --> Loop 48
### Ranking functions of CR start(V,V1,V17,V18)
#### Partial ranking functions of CR start(V,V1,V17,V18)
Computing Bounds
=====================================
#### Cost of chains of inc(V,Out):
* Chain [[19],20]: 1*it(19)+1
Such that:it(19) =< Out
with precondition: [Out>=1,V>=Out]
* Chain [20]: 1
with precondition: [Out=0,V>=0]
#### Cost of chains of le(V,V1,Out):
* Chain [[21],24]: 1*it(21)+1
Such that:it(21) =< V
with precondition: [Out=2,V>=1,V1>=V]
* Chain [[21],23]: 1*it(21)+1
Such that:it(21) =< V1
with precondition: [Out=1,V1>=1,V>=V1+1]
* Chain [[21],22]: 1*it(21)+0
Such that:it(21) =< V1
with precondition: [Out=0,V>=1,V1>=1]
* Chain [24]: 1
with precondition: [V=0,Out=2,V1>=0]
* Chain [23]: 1
with precondition: [V1=0,Out=1,V>=1]
* Chain [22]: 0
with precondition: [Out=0,V>=0,V1>=0]
#### Cost of chains of minus(V,V1,Out):
* Chain [[25],27]: 1*it(25)+1
Such that:it(25) =< V1
with precondition: [Out=0,V>=1,V1>=1]
* Chain [[25],26]: 1*it(25)+1
Such that:it(25) =< V1
with precondition: [V=Out+V1,V1>=1,V>=V1]
* Chain [27]: 1
with precondition: [Out=0,V>=0,V1>=0]
* Chain [26]: 1
with precondition: [V1=0,V=Out,V>=0]
#### Cost of chains of quot(V,V1,Out):
* Chain [[30],31]: 2*it(30)+1
Such that:it(30) =< Out
with precondition: [V1=1,Out>=1,V>=Out]
* Chain [[30],29,31]: 2*it(30)+1*s(3)+3
Such that:s(3) =< 1
it(30) =< Out
with precondition: [V1=1,Out>=2,V>=Out]
* Chain [[28],31]: 2*it(28)+1*s(6)+1
Such that:it(28) =< V-V1+1
aux(3) =< V
it(28) =< aux(3)
s(6) =< aux(3)
with precondition: [V1>=2,Out>=1,V+2>=2*Out+V1]
* Chain [[28],29,31]: 2*it(28)+1*s(3)+1*s(6)+3
Such that:it(28) =< V-V1+1
s(3) =< V1
aux(4) =< V
it(28) =< aux(4)
s(6) =< aux(4)
with precondition: [V1>=2,Out>=2,V+3>=2*Out+V1]
* Chain [31]: 1
with precondition: [Out=0,V>=0,V1>=0]
* Chain [29,31]: 1*s(3)+3
Such that:s(3) =< V1
with precondition: [Out=1,V>=1,V1>=1]
#### Cost of chains of log2(V,V1,Out):
* Chain [[33,35],41]: 12*it(33)+9*it(35)+14*s(10)+3*s(60)+2*s(61)+3*s(65)+5
Such that:aux(6) =< 1
s(66) =< 2*V
aux(18) =< V
aux(19) =< 3*V
s(10) =< aux(6)
it(33) =< aux(18)
it(35) =< aux(18)
it(35) =< aux(19)
s(61) =< aux(18)*2
s(65) =< s(66)
s(60) =< aux(19)
with precondition: [Out=0,V>=2,V1>=0]
* Chain [[33,35],39]: 12*it(33)+9*it(35)+3*s(60)+2*s(61)+3*s(65)+6*s(68)+5
Such that:aux(20) =< 1
s(66) =< 2*V
aux(22) =< V
aux(23) =< 3*V
s(68) =< aux(20)
it(33) =< aux(22)
it(35) =< aux(22)
it(35) =< aux(23)
s(61) =< aux(22)*2
s(65) =< s(66)
s(60) =< aux(23)
with precondition: [Out=0,V>=2,V1>=0]
* Chain [[33,35],37,41]: 12*it(33)+9*it(35)+15*s(10)+3*s(60)+2*s(61)+3*s(65)+12
Such that:aux(24) =< 1
s(66) =< 2*V
aux(25) =< V
aux(26) =< 3*V
s(10) =< aux(24)
it(33) =< aux(25)
it(35) =< aux(25)
it(35) =< aux(26)
s(61) =< aux(25)*2
s(65) =< s(66)
s(60) =< aux(26)
with precondition: [Out=0,V>=3,V1>=0]
* Chain [[33,35],37,40]: 12*it(33)+9*it(35)+3*s(60)+2*s(61)+3*s(65)+3*s(79)+12
Such that:aux(29) =< 1
s(66) =< 2*V
aux(30) =< V
aux(31) =< 3*V
s(79) =< aux(29)
it(33) =< aux(30)
it(35) =< aux(30)
it(35) =< aux(31)
s(61) =< aux(30)*2
s(65) =< s(66)
s(60) =< aux(31)
with precondition: [Out=1,V>=3,V1>=0]
* Chain [[32,34],[33,35],41]: 18*it(32)+18*it(33)+9*it(35)+14*s(10)+3*s(60)+2*s(61)+3*s(110)+1*s(111)+3*s(112)+2*s(113)+2*s(116)+5
Such that:aux(6) =< 1
aux(42) =< V
aux(19) =< 6*V+12*V1
aux(38) =< V1
aux(45) =< 2*V+4*V1
aux(46) =< 3*V
s(10) =< aux(6)
it(33) =< aux(45)
it(35) =< aux(45)
it(35) =< aux(19)
s(61) =< aux(45)*2
s(60) =< aux(19)
aux(36) =< aux(42)
it(32) =< aux(42)
aux(36) =< aux(46)
it(32) =< aux(46)
aux(41) =< aux(38)
s(113) =< aux(36)*2
s(111) =< it(32)*aux(38)
s(110) =< aux(36)
s(120) =< it(32)*aux(41)
s(116) =< s(120)
s(112) =< aux(46)
with precondition: [Out=0,V>=3,V1>=1]
* Chain [[32,34],[33,35],39]: 18*it(32)+18*it(33)+9*it(35)+3*s(60)+2*s(61)+6*s(68)+3*s(110)+1*s(111)+3*s(112)+2*s(113)+2*s(116)+5
Such that:aux(20) =< 1
aux(42) =< V
aux(23) =< 6*V+12*V1
aux(38) =< V1
aux(47) =< 2*V+4*V1
aux(48) =< 3*V
s(68) =< aux(20)
it(33) =< aux(47)
it(35) =< aux(47)
it(35) =< aux(23)
s(61) =< aux(47)*2
s(60) =< aux(23)
aux(36) =< aux(42)
it(32) =< aux(42)
aux(36) =< aux(48)
it(32) =< aux(48)
aux(41) =< aux(38)
s(113) =< aux(36)*2
s(111) =< it(32)*aux(38)
s(110) =< aux(36)
s(120) =< it(32)*aux(41)
s(116) =< s(120)
s(112) =< aux(48)
with precondition: [Out=0,V>=3,V1>=1]
* Chain [[32,34],[33,35],37,41]: 18*it(32)+18*it(33)+9*it(35)+15*s(10)+3*s(60)+2*s(61)+3*s(110)+1*s(111)+3*s(112)+2*s(113)+2*s(116)+12
Such that:aux(24) =< 1
aux(42) =< V
aux(26) =< 6*V+12*V1
aux(38) =< V1
aux(49) =< 2*V+4*V1
aux(50) =< 3*V
s(10) =< aux(24)
it(33) =< aux(49)
it(35) =< aux(49)
it(35) =< aux(26)
s(61) =< aux(49)*2
s(60) =< aux(26)
aux(36) =< aux(42)
it(32) =< aux(42)
aux(36) =< aux(50)
it(32) =< aux(50)
aux(41) =< aux(38)
s(113) =< aux(36)*2
s(111) =< it(32)*aux(38)
s(110) =< aux(36)
s(120) =< it(32)*aux(41)
s(116) =< s(120)
s(112) =< aux(50)
with precondition: [Out=0,V>=5,V1>=1]
* Chain [[32,34],[33,35],37,40]: 18*it(32)+18*it(33)+9*it(35)+3*s(60)+2*s(61)+3*s(79)+3*s(110)+1*s(111)+3*s(112)+2*s(113)+2*s(116)+12
Such that:aux(29) =< 1
aux(42) =< V
aux(31) =< 6*V+12*V1
aux(38) =< V1
aux(51) =< 2*V+4*V1
aux(52) =< 3*V
s(79) =< aux(29)
it(33) =< aux(51)
it(35) =< aux(51)
it(35) =< aux(31)
s(61) =< aux(51)*2
s(60) =< aux(31)
aux(36) =< aux(42)
it(32) =< aux(42)
aux(36) =< aux(52)
it(32) =< aux(52)
aux(41) =< aux(38)
s(113) =< aux(36)*2
s(111) =< it(32)*aux(38)
s(110) =< aux(36)
s(120) =< it(32)*aux(41)
s(116) =< s(120)
s(112) =< aux(52)
with precondition: [Out=1,V>=5,V1>=1]
* Chain [[32,34],41]: 12*it(32)+9*it(34)+14*s(10)+12*s(12)+1*s(111)+3*s(112)+2*s(113)+2*s(116)+5
Such that:aux(6) =< 1
aux(38) =< V1
aux(53) =< V
aux(54) =< 2*V+4*V1
aux(55) =< 3*V
s(10) =< aux(6)
s(12) =< aux(54)
it(32) =< aux(53)
it(34) =< aux(53)
it(34) =< aux(55)
aux(41) =< aux(38)
s(113) =< aux(53)*2
s(111) =< it(32)*aux(38)
s(120) =< it(34)*aux(41)
s(116) =< s(120)
s(112) =< aux(55)
with precondition: [Out=0,V>=2,V1>=1]
* Chain [[32,34],39]: 12*it(32)+9*it(34)+6*s(68)+6*s(70)+1*s(111)+3*s(112)+2*s(113)+2*s(116)+5
Such that:aux(20) =< 1
aux(38) =< V1
aux(56) =< V
aux(57) =< 2*V+4*V1
aux(58) =< 3*V
s(68) =< aux(20)
s(70) =< aux(57)
it(32) =< aux(56)
it(34) =< aux(56)
it(34) =< aux(58)
aux(41) =< aux(38)
s(113) =< aux(56)*2
s(111) =< it(32)*aux(38)
s(120) =< it(34)*aux(41)
s(116) =< s(120)
s(112) =< aux(58)
with precondition: [Out=0,V>=2,V1>=1]
* Chain [[32,34],38]: 12*it(32)+9*it(34)+1*s(111)+3*s(112)+2*s(113)+2*s(116)+4*s(118)+1*s(122)+6
Such that:s(122) =< 1
aux(38) =< V1
aux(59) =< V
aux(60) =< 2*V+4*V1
aux(61) =< 3*V
s(118) =< aux(60)
it(32) =< aux(59)
it(34) =< aux(59)
it(34) =< aux(61)
aux(41) =< aux(38)
s(113) =< aux(59)*2
s(111) =< it(32)*aux(38)
s(120) =< it(34)*aux(41)
s(116) =< s(120)
s(112) =< aux(61)
with precondition: [V>=2,Out>=0,V1>=Out+1]
* Chain [[32,34],37,41]: 12*it(32)+9*it(34)+15*s(10)+1*s(111)+3*s(112)+2*s(113)+2*s(116)+3*s(118)+12
Such that:aux(24) =< 1
s(119) =< 2*V+4*V1
aux(38) =< V1
aux(62) =< V
aux(63) =< 3*V
s(10) =< aux(24)
it(32) =< aux(62)
it(34) =< aux(62)
it(34) =< aux(63)
aux(41) =< aux(38)
s(113) =< aux(62)*2
s(111) =< it(32)*aux(38)
s(120) =< it(34)*aux(41)
s(116) =< s(120)
s(118) =< s(119)
s(112) =< aux(63)
with precondition: [Out=0,V>=3,V1>=1]
* Chain [[32,34],37,40]: 12*it(32)+9*it(34)+3*s(79)+1*s(111)+3*s(112)+2*s(113)+2*s(116)+3*s(118)+12
Such that:aux(29) =< 1
s(119) =< 2*V+4*V1
aux(38) =< V1
aux(64) =< V
aux(65) =< 3*V
s(79) =< aux(29)
it(32) =< aux(64)
it(34) =< aux(64)
it(34) =< aux(65)
aux(41) =< aux(38)
s(113) =< aux(64)*2
s(111) =< it(32)*aux(38)
s(120) =< it(34)*aux(41)
s(116) =< s(120)
s(118) =< s(119)
s(112) =< aux(65)
with precondition: [Out=1,V>=3,V1>=1]
* Chain [[32,34],36,41]: 12*it(32)+9*it(34)+15*s(10)+13*s(12)+1*s(111)+3*s(112)+2*s(113)+2*s(116)+12
Such that:aux(66) =< 1
aux(38) =< V1
aux(68) =< V
aux(69) =< 2*V+4*V1
aux(70) =< 3*V
s(10) =< aux(66)
s(12) =< aux(69)
it(32) =< aux(68)
it(34) =< aux(68)
it(34) =< aux(70)
aux(41) =< aux(38)
s(113) =< aux(68)*2
s(111) =< it(32)*aux(38)
s(120) =< it(34)*aux(41)
s(116) =< s(120)
s(112) =< aux(70)
with precondition: [Out=0,V>=3,V1>=1]
* Chain [[32,34],36,40]: 12*it(32)+9*it(34)+6*s(80)+3*s(81)+1*s(111)+3*s(112)+2*s(113)+2*s(116)+12
Such that:aux(71) =< 1
aux(38) =< V1
aux(73) =< V
aux(74) =< 2*V+4*V1
aux(75) =< 3*V
s(81) =< aux(71)
s(80) =< aux(74)
it(32) =< aux(73)
it(34) =< aux(73)
it(34) =< aux(75)
aux(41) =< aux(38)
s(113) =< aux(73)*2
s(111) =< it(32)*aux(38)
s(120) =< it(34)*aux(41)
s(116) =< s(120)
s(112) =< aux(75)
with precondition: [Out=1,V>=3,V1>=1]
* Chain [41]: 14*s(10)+9*s(12)+5
Such that:aux(6) =< 1
aux(7) =< V1
s(10) =< aux(6)
s(12) =< aux(7)
with precondition: [Out=0,V>=0,V1>=0]
* Chain [40]: 2*s(80)+2*s(81)+5
Such that:aux(27) =< 1
aux(28) =< V1
s(81) =< aux(27)
s(80) =< aux(28)
with precondition: [V=0,Out=1,V1>=0]
* Chain [39]: 6*s(68)+3*s(70)+5
Such that:aux(20) =< 1
aux(21) =< V1
s(68) =< aux(20)
s(70) =< aux(21)
with precondition: [V=1,Out=0,V1>=0]
* Chain [38]: 1*s(122)+1*s(123)+6
Such that:s(122) =< 1
s(123) =< V1
with precondition: [V=1,Out>=0,V1>=Out+1]
* Chain [37,41]: 15*s(10)+12
Such that:aux(24) =< 1
s(10) =< aux(24)
with precondition: [Out=0,V>=2,V1>=0]
* Chain [37,40]: 3*s(79)+12
Such that:aux(29) =< 1
s(79) =< aux(29)
with precondition: [Out=1,V>=2,V1>=0]
* Chain [36,41]: 15*s(10)+10*s(12)+12
Such that:aux(66) =< 1
aux(67) =< V1
s(10) =< aux(66)
s(12) =< aux(67)
with precondition: [Out=0,V>=2,V1>=1]
* Chain [36,40]: 3*s(80)+3*s(81)+12
Such that:aux(71) =< 1
aux(72) =< V1
s(81) =< aux(71)
s(80) =< aux(72)
with precondition: [Out=1,V>=2,V1>=1]
#### Cost of chains of start(V,V1,V17,V18):
* Chain [48]: 33*s(356)+256*s(358)+4*s(363)+381*s(372)+139*s(383)+333*s(385)+42*s(387)+87*s(391)+36*s(392)+8*s(393)+12*s(394)+16*s(396)+24*s(398)+119*s(439)+7*s(444)+22*s(446)+36*s(448)+8*s(449)+12*s(450)+4*s(453)+13
Such that:aux(90) =< 1
aux(91) =< V
aux(92) =< V-V1+1
aux(93) =< 2*V
aux(94) =< 2*V+4*V1
aux(95) =< 3*V
aux(96) =< 6*V
aux(97) =< 6*V+12*V1
aux(98) =< V1
s(372) =< aux(90)
s(358) =< aux(91)
s(363) =< aux(92)
s(356) =< aux(98)
s(383) =< aux(93)
s(385) =< aux(91)
s(385) =< aux(95)
s(387) =< aux(91)*2
s(391) =< aux(95)
s(392) =< aux(93)
s(392) =< aux(96)
s(393) =< aux(93)*2
s(394) =< aux(96)
s(395) =< aux(91)
s(395) =< aux(95)
s(396) =< s(395)*2
s(398) =< s(395)
s(439) =< aux(94)
s(442) =< aux(98)
s(444) =< s(358)*aux(98)
s(445) =< s(385)*s(442)
s(446) =< s(445)
s(448) =< aux(94)
s(448) =< aux(97)
s(449) =< aux(94)*2
s(450) =< aux(97)
s(453) =< s(385)*aux(98)
s(363) =< aux(91)
with precondition: [V>=0]
* Chain [47]: 1612*s(498)+98*s(499)+88*s(509)+27*s(518)+6*s(519)+9*s(520)+28*s(526)+88*s(536)+234*s(538)+28*s(540)+4*s(541)+14*s(543)+60*s(544)+27*s(545)+6*s(546)+9*s(547)+12*s(549)+3*s(550)+18*s(551)+131*s(556)+119*s(568)+132*s(569)+171*s(570)+22*s(572)+7*s(573)+22*s(575)+45*s(576)+36*s(577)+8*s(578)+12*s(579)+8*s(581)+4*s(582)+12*s(583)+119*s(649)+132*s(650)+171*s(651)+22*s(653)+7*s(654)+22*s(656)+45*s(657)+36*s(658)+8*s(659)+12*s(660)+8*s(662)+4*s(663)+12*s(664)+12*s(665)+88*s(727)+27*s(736)+6*s(737)+9*s(738)+88*s(754)+4*s(759)+14*s(761)+27*s(763)+6*s(764)+9*s(765)+3*s(768)+33*s(774)+119*s(786)+132*s(787)+171*s(788)+22*s(790)+7*s(791)+22*s(793)+45*s(794)+36*s(795)+8*s(796)+12*s(797)+8*s(799)+4*s(800)+12*s(801)+119*s(867)+132*s(868)+171*s(869)+22*s(871)+7*s(872)+22*s(874)+45*s(875)+36*s(876)+8*s(877)+12*s(878)+8*s(880)+4*s(881)+12*s(882)+12*s(883)+17
Such that:s(721) =< 4*V17
s(748) =< 4*V17+2
s(723) =< 12*V17
s(750) =< 12*V17+6
s(503) =< 4*V18
s(530) =< 4*V18+2
s(505) =< 12*V18
s(532) =< 12*V18+6
aux(119) =< 1
aux(120) =< 2
aux(121) =< 3
aux(122) =< V1
aux(123) =< V1+1
aux(124) =< V1+4*V17
aux(125) =< V1+4*V17+1
aux(126) =< 3*V1+12*V17
aux(127) =< 3*V1+12*V17+3
aux(128) =< V1/2
aux(129) =< V1/2+1/2
aux(130) =< 3/2*V1
aux(131) =< 3/2*V1+3/2
aux(132) =< V17
aux(133) =< V17+1
aux(134) =< V17+4*V18
aux(135) =< V17+4*V18+1
aux(136) =< 3*V17+12*V18
aux(137) =< 3*V17+12*V18+3
aux(138) =< V17/2
aux(139) =< V17/2+1/2
aux(140) =< 3/2*V17
aux(141) =< 3/2*V17+3/2
aux(142) =< V18
s(498) =< aux(119)
s(526) =< aux(120)
s(556) =< aux(132)
s(499) =< aux(142)
s(509) =< s(503)
s(518) =< s(503)
s(518) =< s(505)
s(519) =< s(503)*2
s(520) =< s(505)
s(568) =< aux(134)
s(569) =< aux(138)
s(570) =< aux(138)
s(570) =< aux(140)
s(539) =< aux(142)
s(572) =< aux(138)*2
s(573) =< s(569)*aux(142)
s(574) =< s(570)*s(539)
s(575) =< s(574)
s(576) =< aux(140)
s(577) =< aux(134)
s(577) =< aux(136)
s(578) =< aux(134)*2
s(579) =< aux(136)
s(580) =< aux(138)
s(580) =< aux(140)
s(581) =< s(580)*2
s(582) =< s(570)*aux(142)
s(583) =< s(580)
s(649) =< aux(135)
s(650) =< aux(139)
s(651) =< aux(139)
s(651) =< aux(141)
s(653) =< aux(139)*2
s(654) =< s(650)*aux(142)
s(655) =< s(651)*s(539)
s(656) =< s(655)
s(657) =< aux(141)
s(658) =< aux(135)
s(658) =< aux(137)
s(659) =< aux(135)*2
s(660) =< aux(137)
s(661) =< aux(139)
s(661) =< aux(141)
s(662) =< s(661)*2
s(663) =< s(651)*aux(142)
s(664) =< s(661)
s(665) =< aux(133)
s(727) =< s(721)
s(736) =< s(721)
s(736) =< s(723)
s(737) =< s(721)*2
s(738) =< s(723)
s(774) =< aux(122)
s(786) =< aux(124)
s(787) =< aux(128)
s(788) =< aux(128)
s(788) =< aux(130)
s(757) =< aux(132)
s(790) =< aux(128)*2
s(791) =< s(787)*aux(132)
s(792) =< s(788)*s(757)
s(793) =< s(792)
s(794) =< aux(130)
s(795) =< aux(124)
s(795) =< aux(126)
s(796) =< aux(124)*2
s(797) =< aux(126)
s(798) =< aux(128)
s(798) =< aux(130)
s(799) =< s(798)*2
s(800) =< s(788)*aux(132)
s(801) =< s(798)
s(867) =< aux(125)
s(868) =< aux(129)
s(869) =< aux(129)
s(869) =< aux(131)
s(871) =< aux(129)*2
s(872) =< s(868)*aux(132)
s(873) =< s(869)*s(757)
s(874) =< s(873)
s(875) =< aux(131)
s(876) =< aux(125)
s(876) =< aux(127)
s(877) =< aux(125)*2
s(878) =< aux(127)
s(879) =< aux(129)
s(879) =< aux(131)
s(880) =< s(879)*2
s(881) =< s(869)*aux(132)
s(882) =< s(879)
s(883) =< aux(123)
s(536) =< s(530)
s(538) =< aux(119)
s(538) =< aux(121)
s(540) =< aux(119)*2
s(541) =< s(498)*aux(142)
s(542) =< s(538)*s(539)
s(543) =< s(542)
s(544) =< aux(121)
s(545) =< s(530)
s(545) =< s(532)
s(546) =< s(530)*2
s(547) =< s(532)
s(548) =< aux(119)
s(548) =< aux(121)
s(549) =< s(548)*2
s(550) =< s(538)*aux(142)
s(551) =< s(548)
s(754) =< s(748)
s(759) =< s(498)*aux(132)
s(760) =< s(538)*s(757)
s(761) =< s(760)
s(763) =< s(748)
s(763) =< s(750)
s(764) =< s(748)*2
s(765) =< s(750)
s(768) =< s(538)*aux(132)
with precondition: [V=1,V1>=0,V17>=0]
* Chain [46]: 1*s(932)+1*s(933)+6
Such that:s(932) =< 1
s(933) =< V1
with precondition: [V=1,V1>=1]
* Chain [45]: 1
with precondition: [V=2,V1>=0,V17>=0,V18>=0]
* Chain [44]: 1
with precondition: [V=2,V1>=0,V17>=1]
* Chain [43]: 1
with precondition: [V1=0,V>=0]
* Chain [42]: 1*s(934)+4*s(936)+3
Such that:s(934) =< 1
s(935) =< V
s(936) =< s(935)
with precondition: [V1=1,V>=1]
Closed-form bounds of start(V,V1,V17,V18):
-------------------------------------
* Chain [48] with precondition: [V>=0]
- Upper bound: 729*V+394+nat(V1)*33+nat(V1)*33*V+382*V+261*V+72*V+nat(2*V+4*V1)*171+nat(6*V+12*V1)*12+nat(V-V1+1)*4
- Complexity: n^2
* Chain [47] with precondition: [V=1,V1>=0,V17>=0]
- Upper bound: 33*V1+152*V17+2197+ (V1/2+1/2)* (33*V17)+V1/2* (33*V17)+nat(V18)*119+ (V17/2+1/2)* (nat(V18)*33)+V17/2* (nat(V18)*33)+508*V17+nat(4*V18)*127+108*V17+nat(12*V18)*9+135/2*V1+135/2*V17+ (12*V1+12)+ (171*V1+684*V17)+ (12*V17+12)+nat(V17+4*V18)*171+ (36*V1+144*V17)+nat(3*V17+12*V18)*12+ (508*V17+254)+nat(4*V18+2)*127+ (108*V17+54)+nat(12*V18+6)*9+ (135/2*V1+135/2)+ (135/2*V17+135/2)+ (171*V1+684*V17+171)+nat(V17+4*V18+1)*171+ (36*V1+144*V17+36)+nat(3*V17+12*V18+3)*12+ (375/2*V1+375/2)+ (375/2*V17+375/2)+375/2*V1+375/2*V17
- Complexity: n^2
* Chain [46] with precondition: [V=1,V1>=1]
- Upper bound: V1+7
- Complexity: n
* Chain [45] with precondition: [V=2,V1>=0,V17>=0,V18>=0]
- Upper bound: 1
- Complexity: constant
* Chain [44] with precondition: [V=2,V1>=0,V17>=1]
- Upper bound: 1
- Complexity: constant
* Chain [43] with precondition: [V1=0,V>=0]
- Upper bound: 1
- Complexity: constant
* Chain [42] with precondition: [V1=1,V>=1]
- Upper bound: 4*V+4
- Complexity: n
### Maximum cost of start(V,V1,V17,V18): max([4*V+3,nat(V1)*32+387+max([nat(V1)*33*V+729*V+382*V+261*V+72*V+nat(2*V+4*V1)*171+nat(6*V+12*V1)*12+nat(V-V1+1)*4,nat(V17)*152+1803+nat(V17)*33*nat(V1/2+1/2)+nat(V17)*33*nat(V1/2)+nat(V18)*119+nat(V18)*33*nat(V17/2+1/2)+nat(V18)*33*nat(V17/2)+nat(4*V17)*127+nat(4*V18)*127+nat(12*V17)*9+nat(12*V18)*9+nat(3/2*V1)*45+nat(3/2*V17)*45+nat(V1+1)*12+nat(V1+4*V17)*171+nat(V17+1)*12+nat(V17+4*V18)*171+nat(3*V1+12*V17)*12+nat(3*V17+12*V18)*12+nat(4*V17+2)*127+nat(4*V18+2)*127+nat(12*V17+6)*9+nat(12*V18+6)*9+nat(3/2*V1+3/2)*45+nat(3/2*V17+3/2)*45+nat(V1+4*V17+1)*171+nat(V17+4*V18+1)*171+nat(3*V1+12*V17+3)*12+nat(3*V17+12*V18+3)*12+nat(V1/2+1/2)*375+nat(V17/2+1/2)*375+nat(V1/2)*375+nat(V17/2)*375])+ (nat(V1)+6)])+1
Asymptotic class: n^2
* Total analysis performed in 2079 ms.